package probsym;

import gov.nasa.jpf.symbc.Debug;

/*
 * Taken from Figure 1 on p. 65 of
 * 
 * Ferguson, Korel: The Chaining Approach for Software Test Data Generation, ACM Transactions on Software Engineering an dMethodology, volume 5, Number 1, January 1996, pp. 63--86.
 */

class Chaining {

	public static void sample(int[] a, int[] b, int target) {
		int len = a.length;
		int i = 1;
		boolean fa = false;
		boolean fb = false;
		while (i < len) {
			if (a[i] == target) {
				fa = true;
			}
			i++;
		}
		if (fa) {
			i = 1;
			fb = true;
			while (i < len) {
				if (b[i] != target) {
					fb = false;
				}
				i++;
			}
		}
		if (fb) {
			System.out.println("Message 1");
		} else {
			System.out.println("Message 2");
		}
	}

	public static void runTestDriver(int length) {
		int[] a = new int[length];
		int[] b = new int[length];
		for (int i = 0; i < length; i++) {
			a[i] = Debug.makeSymbolicInteger("a" + i);
			b[i] = Debug.makeSymbolicInteger("b" + i);
		}
	    sample(a, b, Debug.makeSymbolicInteger("target"));
	}
	
	public static void main(String[] Argv) {
		runTestDriver(4);
	}

}
